/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30



␈↓ ↓H␈↓␈↓ ∧r␈↓αCORRECTNESS OF ␈↓↓samefringe␈↓

␈↓ ↓H␈↓␈↓ α_We make the following LISP definitions:

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓fringe x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x␈↓,

␈↓ ↓H␈↓where ␈↓↓u * v␈↓ denotes ␈↓↓append[u,v]␈↓ and satisfies

␈↓ ↓H␈↓2)␈↓ α8 ␈↓↓u * v ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓,

␈↓ ↓H␈↓3)␈↓ α8  ␈↓↓samefringe[x,y] ← x ␈↓αeq␈↓↓ y ∨ [¬␈↓αat␈↓↓ x ∧ ¬␈↓αat␈↓↓ y ∧ same[gopher x, gopher y]␈↓,

␈↓ ↓H␈↓4)␈↓ α8  ␈↓↓same[x,y] ← ␈↓αa␈↓↓ x ␈↓αeq␈↓↓ ␈↓αa␈↓↓ y ∧ samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]␈↓,

␈↓ ↓H␈↓and

␈↓ ↓H␈↓5)␈↓ α8  ␈↓↓gopher x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ gopher[␈↓αaa␈↓↓ x . [␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x]]␈↓.

␈↓ ↓H␈↓␈↓ α_␈↓↓fringe␈αx␈↓,␈αwhich␈αwas␈αcalled␈α␈↓↓flatten␈αx␈↓␈αin␈αthe␈α␈↓↓Course␈αNotes␈↓,␈αgives␈αa␈αlist␈αof␈αthe␈αatoms␈αin␈αthe␈αS-
␈↓ ↓H␈↓expression␈α⊂␈↓↓x␈↓.␈α⊂ Thus␈α⊂␈↓↓fringe␈↓[((A.B).C)] = (A B C).␈α⊂ We␈α⊂also␈α⊂have␈α⊃␈↓↓fringe␈↓[(A.(B.C))] = (A B C),␈α⊂so
␈↓ ↓H␈↓that different S-expressions can have the same fringe.  Indeed our object is to prove

␈↓ ↓H␈↓␈↓αTheorem 1␈↓ - ␈↓↓∀x y.(samefringe[x,y] ≡ fringe x = fringe y␈↓).

␈↓ ↓H␈↓␈↓ α_␈↓↓samefringe␈↓␈α∂and␈α∂␈↓↓same␈↓␈α∂are␈α∂mutually␈α∂recursive␈α∞LISP␈α∂predicates,␈α∂and␈α∂␈↓↓gopher␈↓␈α∂is␈α∂an␈α∞auxiliary
␈↓ ↓H␈↓function␈αthat␈αdigs␈αout␈αthe␈αfirst␈αatom␈αof␈αan␈αS-expression␈αpiling␈αwhatever␈αelse␈αit␈αmeets␈αonto␈αthe␈α␈↓↓cdr␈↓
␈↓ ↓H␈↓part of the expression.  Thus ␈↓↓gopher␈↓[(((A.B).(C.D)).(E.F))] = (A.(B.((C.D).(E.F)))).

␈↓ ↓H␈↓␈↓ α_The␈α∂proof␈α∂is␈α∂divided␈α∂into␈α∂five␈α∂parts.␈α∂ First␈α∂we␈α∂convert␈α∂the␈α∂recursive␈α∂programs␈α∂into␈α∂first
␈↓ ↓H␈↓order␈αlogic␈αfunctional␈αequations.␈α ␈↓↓fringe␈↓␈αand␈α␈↓↓gopher␈↓␈αconvert␈αeasily,␈αbut␈αsince␈α␈↓↓samefringe␈↓␈αand␈αsame
␈↓ ↓H␈↓are␈α⊃predicates,␈α⊃they␈α⊃must␈α⊃be␈α⊃expressed␈α⊃in␈α⊃terms␈α⊃of␈α⊃pseudo-predicates␈α⊃␈↓↓samefringea␈↓␈α∩and␈α⊃␈↓↓samea␈↓
␈↓ ↓H␈↓which have functional equations using the pseudo-propositional connnectives.

␈↓ ↓H␈↓␈↓ α_Next␈α∩we␈α∩prove␈α∩that␈α∩␈↓↓fringe␈↓␈α∩and␈α∪␈↓↓gopher␈↓␈α∩are␈α∩total␈α∩and␈α∩prove␈α∩some␈α∩lemmas␈α∪about␈α∩their
␈↓ ↓H␈↓properties.  These proofs are straightforward structural inductions.

␈↓ ↓H␈↓␈↓ α_Next␈αwe␈αprove␈αthat␈αthat␈α␈↓↓samefringea␈↓␈αis␈αtotal.␈α The␈αproof␈αis␈αa␈αcourse-of-values␈αinduction␈α
on
␈↓ ↓H␈↓␈↓↓size x + size y␈↓.

␈↓ ↓H␈↓␈↓ α_From␈α
this␈αwe␈α
show␈α
that␈αthe␈α
predicates␈α␈↓↓samefringe␈↓␈α
and␈α
␈↓↓same␈↓␈αsatisfy␈α
their␈αrecursion␈α
equations
␈↓ ↓H␈↓using genuine propositional connectives.

␈↓ ↓H␈↓␈↓ α_Finally,␈α
we␈α
show␈αthat␈α
the␈α
predicate␈α
␈↓↓fringe␈αx␈α
=␈α
fringe␈α
y␈↓␈αsatisfies␈α
the␈α
functional␈α
equation␈αof
␈↓ ↓H␈↓␈↓↓samefringe[x,y]␈↓.␈α Since␈α␈↓↓samefringe␈↓␈αhas␈αbeen␈αproved␈αtotal,␈αthis␈αallows␈αuse␈αto␈αuse␈αthe␈αminimization
␈↓ ↓H␈↓schema of ␈↓↓samefringe␈↓ to conclude the theorem.

␈↓ ↓H␈↓Part 1

␈↓ ↓H␈↓␈↓ α_Equations (1) to (5) become
␈↓ ↓H␈↓␈↓ εH␈↓ 91


␈↓ ↓H␈↓6)␈↓ α8  ␈↓↓∀x.[fringe x = ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x * fringe ␈↓αd␈↓↓ x]␈↓,

␈↓ ↓H␈↓7)␈↓ α8  ␈↓↓∀u v.[u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]]␈↓,

␈↓ ↓H␈↓8)␈↓ α8  ␈↓↓∀x y.[samefringe[x,y] ≡ [samefringea[x,y] = T]]␈↓,

␈↓ ↓H␈↓9)␈↓ α8␈α ␈↓↓∀x␈αy.[samefringea[x,y]␈α=␈α[x␈α=␈αy]␈αor␈α[not␈αaatom␈αx␈αand␈αnot␈αaatom␈αy␈αand␈αsamea[gopher␈αx,
␈↓ ↓H␈↓↓gopher y]]␈↓,

␈↓ ↓H␈↓10)␈↓ α8  ␈↓↓∀x y.[same[x,y] ≡ [samea[x,y] = T]]␈↓,

␈↓ ↓H␈↓11)␈↓ α8 ␈↓↓∀x y.[samea[x,y] = [␈↓αa␈↓↓ x = ␈↓αa␈↓↓ y] and samefringe[␈↓αd␈↓↓ x, ␈↓αd␈↓↓ y]]␈↓,

␈↓ ↓H␈↓and

␈↓ ↓H␈↓12)␈↓ α8 ␈↓↓∀x.[gopher x = ␈↓αif␈↓↓ ␈↓αat␈↓↓ ␈↓αa␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ gopher[␈↓αaa␈↓↓ x.[␈↓αda␈↓↓ x . ␈↓αd␈↓↓ x]]]␈↓.

␈↓ ↓H␈↓␈↓ α_Notice␈α
that␈α
the␈α
recursively␈α
defined␈α
predicates␈α␈↓↓samefringe␈↓␈α
and␈α
␈↓↓same␈↓␈α
must␈α
be␈α
defined␈αin␈α
terms
␈↓ ↓H␈↓of␈α⊂the␈α∂pseudo-predicates␈α⊂␈↓↓samefringea␈↓␈α∂and␈α⊂␈↓↓same␈↓␈α∂in␈α⊂order␈α∂to␈α⊂legitimately␈α∂translate␈α⊂the␈α∂recursion
␈↓ ↓H␈↓equations into first order formulas.

␈↓ ↓H␈↓␈↓αLemmas about ␈↓↓gopher␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α∞first␈α∞lemma␈α∞is␈α∞that␈α∞␈↓↓gopher␈↓␈α∞is␈α∞total␈α∞provided␈α∞its␈α∞argument␈α∞is␈α∞not␈α∞atomic.␈α∂ Since␈α∞every
␈↓ ↓H␈↓non-atom is the result of a ␈↓↓cons␈↓, we can express this assertion in the form

␈↓ ↓H␈↓Lemma 1: ␈↓↓∀x y.(issexp gopher[x.y])␈↓.

␈↓ ↓H␈↓It is proved by simple S-expression induction on the sentence

␈↓ ↓H␈↓13)␈↓ α8 ␈↓↓qF[x] ≡ ∀y.issexp gopher[x.y]␈↓,

␈↓ ↓H␈↓The general induction statement

␈↓ ↓H␈↓14)␈↓ α8 ∀x.(␈↓αat␈↓ x ⊃ qF[x]) ∧ ∀x.(¬␈↓αat␈↓ x ∧ qF[␈↓αa␈↓ x] ∧ qF[␈↓αd␈↓ x] ⊃ qF[x]) ⊃ ∀x.qF[x]

␈↓ ↓H␈↓then takes the form

␈↓ ↓H␈↓15)␈↓ α8␈α
␈↓↓∀x.(␈↓αat␈↓↓␈α
x␈α
⊃␈α
∀y.issexp␈α∞gopher[x.y])␈α
∧␈α
∀x.(¬␈↓αat␈↓↓␈α
x␈α
∧␈α∞∀y.issexp␈α
gopher[␈↓αa␈↓↓␈α
x␈α
.␈α
y]␈α∞∧␈α
∀y.issexp
␈↓ ↓H␈↓↓gopher[␈↓αd␈↓↓ x . y] ⊃ ∀y.issexp gopher[x.y]) ⊃ ∀x ∀y.issexp gopher[x.y]␈↓.

␈↓ ↓H␈↓The␈α
conclusion␈α
of␈α
(15)␈α
is␈α
our␈α
goal.␈α
 Therefore␈α
we␈α
must␈α
establish␈α
its␈α
premisses.␈α
 Each␈α
of␈α
the␈α
two
␈↓ ↓H␈↓premisses␈αis␈αan␈αimplication␈αuniversally␈αquantified␈αon␈α␈↓↓x␈↓␈αwith␈α␈↓↓∀y.issexp␈αgopher[x.y]␈↓␈αas␈αa␈αconclusion
␈↓ ↓H␈↓but␈αwith␈αdifferent␈αpremisses.␈α Thus␈αwe␈αmust␈αestablish␈α␈↓↓∀y.issexp␈αgopher[x.y]␈↓␈αunder␈αthe␈αhypothesis
␈↓ ↓H␈↓␈↓↓␈↓αat␈↓↓␈α8x␈↓␈α7and␈α8again␈α8under␈α7the␈α8hypothesis␈α8␈↓↓¬␈↓αat␈↓↓ x␈α7∧ ∀y.issexp gopher[␈↓αa␈↓↓ x . y]
␈↓ ↓H␈↓↓∧ ∀y.issexp gopher[␈↓αd␈↓↓ x . y]␈↓.  In the atomic case we compute as follows:

␈↓ ↓H␈↓16)␈↓ α8 ␈↓↓issexp gopher[x.y] ≡ issexp[␈↓αif␈↓↓ ␈↓αat␈↓↓ ␈↓αa␈↓↓ [x.y] ␈↓αthen␈↓↓ x.y ␈↓αelse␈↓↓ gopher[␈↓αaa␈↓↓[x.y].[␈↓αda␈↓↓[x.y].␈↓αd␈↓↓[x.y]]]

␈↓ ↓H␈↓↓␈↓ α_≡ ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ issexp[x.y] ␈↓αelse␈↓↓ issexp gopher[␈↓αa␈↓↓ x.[␈↓αd␈↓↓ x. y]]
␈↓ ↓H␈↓␈↓ εH␈↓ 92


␈↓ ↓H␈↓↓␈↓ α_≡ issexp[x.y]

␈↓ ↓H␈↓↓␈↓ α_≡ ␈↓αtrue␈↓.

␈↓ ↓H␈↓↓The␈αfirst␈αequivalence␈αis␈αestablished␈αby␈αsubstituting␈α
x.y␈↓␈αfor␈α␈↓↓x␈↓␈αin␈α(12),␈αthe␈αfirst␈αorder␈α
characterization
␈↓ ↓H␈↓of␈α␈↓↓gopher␈↓.␈α The␈α
second␈αfollows␈αby␈α
distributing␈αthe␈αpredicate␈α
␈↓↓issexp␈↓␈αinto␈αthe␈αconditional␈α
expression
␈↓ ↓H␈↓and␈αsome␈αsimplification␈αbased␈αon␈αthe␈αalgebraic␈αrelations␈αamong␈αthe␈αLISP␈αfunctions.␈α Next␈αwe␈αuse
␈↓ ↓H␈↓the␈αfact␈αthat␈α␈↓↓x␈↓␈αis␈αassumed␈α
atomic,␈αand␈αfinally␈αwe␈αuse␈αaxiom␈α
L8␈αasserting␈αthat␈αthe␈α␈↓↓cons␈↓␈αof␈α
two␈αS-
␈↓ ↓H␈↓expressions␈α∞is␈α∞an␈α∞S-expression.␈α∞ Since␈α∞␈↓↓y␈↓␈α∞was␈α∞not␈α∞subjected␈α∞to␈α∞any␈α∞conditions,␈α∞we␈α∞are␈α∂entitled␈α∞to
␈↓ ↓H␈↓write␈α→␈↓↓∀y.issexp␈α_gopher[x.y]␈↓␈α→and␈α_then␈α→to␈α→discharge␈α_assumption␈α→that␈α_␈↓↓x␈↓␈α→is␈α→atomic␈α_getting
␈↓ ↓H␈↓␈↓↓␈↓αat␈↓↓ x ⊃ ∀y.issexp gopher[x.y]␈↓, and since ␈↓↓x␈↓ wasn't subjected to conditions, we can finally write

␈↓ ↓H␈↓17)␈↓ α8 ␈↓↓∀x.(␈↓αat␈↓↓ x ⊃ ∀y.issexp gopher[x.y])␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α
non-atomic␈α
case␈α
is␈α
similar.␈α
 The␈α∞first␈α
steps␈α
are␈α
as␈α
before␈α
but␈α
we␈α∞continue␈α
differently.
␈↓ ↓H␈↓Thus

␈↓ ↓H␈↓␈↓↓issexp gopher[x.y] ≡ ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ issexp[x.y] ␈↓αelse␈↓↓ issexp gopher[␈↓αa␈↓↓ x.  [␈↓αd␈↓↓ x . y]]

␈↓ ↓H␈↓↓␈↓ α_≡ issexp gopher[␈↓αa␈↓↓ x.[␈↓αd␈↓↓ x.y]]

␈↓ ↓H␈↓↓␈↓ α_≡ ␈↓αtrue␈↓,

␈↓ ↓H␈↓↓where␈α
the␈α
last␈α
step␈αis␈α
justified␈α
by␈α
the␈α
induction␈αhypothesis.␈α
 The␈α
steps␈α
that␈α
introduce␈αthe␈α
implication
␈↓ ↓H␈↓↓signs and quantify are the same as in the atomic case, so that

␈↓ ↓H␈↓↓18)␈↓ α8 ∀x.(¬␈↓αat␈↓↓ x ∧ ∀y.issexp gopher[␈↓αa␈↓↓ x, y] ∧ ∀y.issexp gopher[␈↓αd␈↓↓ x,y] ⊃ ∀y.issexp gopher[x.y])␈↓

␈↓ ↓H␈↓from which Lemma 1 follows.

␈↓ ↓H␈↓Lemma 2: ␈↓↓∀x y. ¬␈↓αat␈↓↓ gopher[x.y] ∧ ␈↓αat␈↓↓ ␈↓αa␈↓↓ gopher[x.y]␈↓.

␈↓ ↓H␈↓Proof: